Specification tree-buffer-asm

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

data asm specification 
   tree_buffer

   using list-prefixn


   

   
   
   
   
   procedures tree_buffer_init# nat :  : nat × list  ;
              tree_buffer_add# elem : list nonfunctional ;
              tree_buffer_get# nat × list :  : list  ;
   variables  h : nat;
              xs : list;
   
   

   

   state variables  h : nat;
                    xs : list;

   initialization procedure tree_buffer_init#

   

   sequential

      
   
      

   

   

   

   

   

   

   

   

   

   

   declarations init:tree_buffer_init#(n; ; h, xs)  precondition n > 0;{h := n, xs := []}
                add:tree_buffer_add#(a; xs){xs := a + xs}
                get:tree_buffer_get#(h, xs; ; x){x := prefixn(h, xs)}
end data asm specification